
\emph{Session types} 
offer a powerful type-theoretic foundation
for the analysis of 
complex 
scenarios of structured communications, as frequently found in service-oriented systems.  
They abstract communication protocols as basic interaction patterns, which 
may then be %are then statically 
checked against specifications\done\todo[C11.]{Fixed (dropped statically), pls check.}
in some core programming calculus ---typ\-i\-cal\-ly, a variant of the $\pi$-calculus~\cite{DBLP:journals/iandc/MilnerPW92a}. 
Introduced in~\cite{DBLP:conf/concur/Honda93,DBLP:conf/esop/HondaVK98}, 
session type theories 
%have received much attention and 
have been extended in multiple directions 
%two notable such extensions concern asynchronous and multiparty communications~(see, e.g.,~\cite{DBLP:conf/forte/KouzapasYH11} and~\cite{DBLP:conf/popl/HondaYC08}, respectively).
%(
---see~\cite{DBLP:conf/wsfm/Dezani-Ciancaglinid09} for a 
%detailed 
survey.
\done\todo[A5.]{Here we have mentioned extensions of session types, such as asynchronous
\cite{DBLP:conf/forte/KouzapasYH11} 
and multiparty
\cite{DBLP:conf/popl/HondaYC08}, as requested by the reviewer.}Their 
%The
practical relevance 
%of session types 
is witnessed by, e.g., 
 their 
 successful 
 application to the analysis of 
 %parallel programs~\cite{DBLP:conf/tools/NgYH12}.
 collaborative, distributed workflows in healthcare services~\cite{DBLP:conf/fhies/HenriksenNHYH12}.

In spite of these developments, 
we find that existing process frameworks based on ses\-sion types
do not adequately support 
%for reasoning about 
mechanisms for 
\emph{runtime adaptation}. 
%Adaptation and evolvability are increasingly relevant issues nowadays, 
%Runtime adaptation is an increasingly relevant issue nowadays, 
As distributed systems and applications are  being deployed in
open, highly dynamic infrastructures (such as cloud computing platforms),
%In such settings,  
runtime adaptation %and dynamic reconfiguration  
appears as a key feature to
ensure continued system operation,
reduce costs, and achieve
business agility.\done\todo[A4.]{J: We have expanded a bit on what we mean by runtime adaptation, but without using~\cite{DBLP:conf/fase/BruniCGLV12} as a reference.}
%More precisely, w
We understand runtime adaptation 
as the dynamic modification of (the behavior of) the system  %residing in a distinguished location 
as a response to an exceptional external event. %, external to the system. 
Even if such events may not be catastrophic, they are often hard to predict.
The initial system specification must explicitly describe the sub-systems amenable to adaptation and their exceptional events. 
Then, on the basis of this initial specification and its projected evolution, 
an array of possible  adaptation routines is defined at design time. 
Runtime adaptation then denotes potential behavior, in the sense that 
a given adaptation routine is triggered only if its associated exceptional event takes place.
While channel mobility  %~\cite{DBLP:journals/entcs/YoshidaV07}) 
present in session languages (commonly referred to as \emph{delegation})
is useful to specify distribution of processing via types~\cite{DBLP:conf/esop/HondaVK98}, 
%dynamic reconfiguration, 
we find that runtime adaptation, %, evolvability, and code update
%are not expressible or are 
in the sense just discussed, 
is hard to specify and reason about in those languages.\done\todo[A2.]{J: We have relaxed this sentence.}


%%possibility of dynamically replacing the behavior of a located process with a new session process that is in some sense ``compatible'' with the old behavior.
%the enhancement of process specifications with update routines which contain information for  potentially enabling reconfiguration actions at runtime. 
%While the information for such routines can be anticipated, 
%the exact conditions and timing for such actions cannot be fully predicted, but it is important to ensure that the code embedded in such update is well-typed.


We thus observe %a rather unfortunate discrepancy
a substantial gap\done\todo[A3.]{J: It was "a rather unfortunate discrepancy"} between 
(i)~the adaptation capabilities of %modern 
communication-based systems in practice, and 
(ii)~the forms of interaction available in existing
%the calculi upon which session types disciplines are defined.
(typed) process frameworks developed to reason about the correctness of such systems.


In this paper we propose an alternative for 
%elementary approach to 
filling in this gap. 
%overcome this discrepancy.
We %extend an existing 
introduce a
session type discipline 
for a language
equipped
with 
mechanisms for runtime adaptation.
Rather than developing yet another session type discipline \emph{from scratch}, we have deliberately 
preferred to build upon existing lines of work. 
Our proposal 
builds upon
%results from combining 
the framework of 
\emph{adaptable processes}, 
an attempt for enhancing process calculi specifications with evolvability mechanisms
which we have developed together with Bravetti and Zavattaro in~\cite{BGPZFMOODS}.
We combine the constructs for adaptable processes with
the main insights %principles %underlying the discipline 
of the session type system
put forward by Garralda et al.~\cite{DBLP:conf/ppdp/GarraldaCD06} for the Boxed Ambient calculus~\cite{DBLP:journals/toplas/BugliesiCC04}.
Since the type system in~\cite{DBLP:conf/ppdp/GarraldaCD06} does not support delegation, 
we incorporate this key mechanism by relying on the ``liberal'' typing system developed by 
Yoshida and Vasconcelos in~\cite{DBLP:journals/entcs/YoshidaV07}.
As a result of this integration of concepts, 
we obtain a simple yet expressive model 
of structured communications with explicit mechanisms for runtime adaptation.


We briefly describe our approach and results. 
Our process language includes
the usual $\pi$-calculus constructs for session communication, but extended 
with the \emph{located processes} and the \emph{update processes} introduced in~\cite{BGPZFMOODS}.
Given a location $l$, a process $P$, and a context $Q$ 
(i.e. a process with zero or more free occurrences of variable $\mathsf{X}$), these two processes are noted $l[P]$ and 
$\adapt{l}{Q}{\mathsf{X}}$, respectively\done\todo[B1.]{The reviewer suggests to change this notation, using abstractions. We have used the notation for abstractions in Davide's book.}. 
%$l\{Q(\mathsf{X})\}$, resp. 
They may synchronize on $l$ so as to evolve into process 
$Q\subst{P}{\mathsf{X}}$ ---the process $Q$ in which all free occurrences of $\mathsf{X}$ are replaced with $P$.
This interaction represents the \emph{update} of  process $P$ at $l$ with an \emph{adaptation routine}
embodied by $Q$, thus realizing the vision of runtime adaptation hinted at above. 
Locations can be nested and are transparent:
within $l[P]$, process $P$ may evolve autonomously, with the potential of interacting with some %neighboring 
update process for $l$. 
%Context $Q$ can be seen as a built-in adaptation mechanism.
%$l\{Q(\mathsf{X})\}$, 
%$\adapt{l}{Q}{X}$,
%as just described, 

%Hence, 
In our language, communicating behavior coexists with update actions. 
This raises the need for disciplining both forms of interaction, in  a way such that protocol abstractions\done\todo[B22.]{I think this doesn't apply}
 given by session types are respected and  evolvability requirements are enforced. 
To this end, by observing that %exploiting the fact that 
our update actions are a simple form of (higher-order) process mobility~\cite{San923}, 
we draw inspiration from the session types 
in~\cite{DBLP:conf/ppdp/GarraldaCD06}, 
which ensure that
sessions within Ambient hierarchies %are \emph{safe}, i.e., they 
are never disrupted by Ambient mobility steps.
By generalizing this insight to the context of (session) processes which execute
in arbitrary, possibly nested locations, we obtain a property which we call \emph{consistency}:
update actions over located processes which are engaged in active session behavior cannot be enabled.

%While both Ambients and adaptable processes rely on nested located processes,
%Ambient mobility and evolvability steps are conceptually very different.
%In fact, %is a major difference:
%Ambient mobility is only defined in a parent-child style, whereas
%located processes and update actions 
% may interact independently of their relative position in the hierarchy induced by location nesting.
%This way, integrating our calculus for adaptable processes %of~\cite{BGPZFMOODS} 
%with the session types discipline in~\cite{DBLP:conf/ppdp/GarraldaCD06}
%roughly amounts to: 

To show how
located and update processes fit in a session-typed process language, 
and to illustrate our  notion of consistency, 
we  consider a simple distributed client/server scenario,
% of distributed, interacting services (a client $C_1$ and a replicated service $S$), 
conveniently represented as located processes:
\begin{eqnarray*}
\mathsf{Sys} & \triangleq &  %\scomponent{l_{0}}{C_1} \para 
\scomponent{l_{1}}{C_1} \para\bigscomponent{l_2}{\scomponent{r}{S} \para R \, } \quad\text{where:} \vspace{3mm} \\ 
C_1  &  \triangleq  & \nopenr{a}{x}.\outC{x}{\mathrm{u_1},\mathrm{p_1}}.\select{x}{n_1.P_1}.\close{x} \\
S  &  \triangleq  & \repopen{a}{y}.\inC{y}{u,p}.\branch{y}{n_1{:}Q_1.\close{y}  \alte n_2{:}Q_2.\close{y}}
\end{eqnarray*}
Intuitively, 
$\mathsf{Sys}$ 
consists of a replicated server $S$ and a client $C_1$, hosted in different locations $r$ and $l_1$, respectively.\done\todo[B23.]{Changed order of $r$ and $l_1$, check.}
Process  $R$, in location $l_2$, represents the platform in which  $S$ is deployed.
The client $C_1$ and the (persistent) server $S$ may synchronize on name $a$ to establish a new session. %of type $\sigma$ 
%between $S$ and $C_1$ %($i \in \{0, 1\}$) 
After that,  
the client first sends its credentials to the server; then, she chooses\done\todo[B24.]{Fixed, although not in the way suggested.} one of the two
labeled alternatives offered by the server. 
Above, 
client $C_1$ selects the alternative on label $n_1$; 
the subsequent client and server behaviors are  abstracted by processes $P_1$ and $Q_1$, respectively.
%(resp. $P_1$ and $Q_1$), 
%which are left unspecified.
Finally, server and client synchronize to close the session.


Starting from $\mathsf{Sys}$, let us suppose that a new session is indeed established by synchronization on $a$. 
Our semantics decrees 
a reduction step $\mathsf{Sys} \pired \mathsf{Sys}'$:
%the following reduction step:  %We then have
\begin{eqnarray*}
\mathsf{Sys}' \!\!\!& = & \!\!\!\! (\nu \kappa)\big(\scomponent{l_{1}}{\outC{\kappa^{+}}{\mathrm{u_1},\mathrm{p_1}}.\select{\kappa^{+}}{n_1.P_1}.\close{\kappa^{+}}} \para \\ 
& & \qquad \bigscomponent{l_2}{\scomponent{r}{\inC{\kappa^{-}}{u,p}.\branch{\kappa^{-}}{n_1{:}Q_1.\close{\kappa^{-}} \alte n_2{:}Q_2.\close{\kappa^{-}}}\,} \para R \, }\big)
\end{eqnarray*} 
where 
$\kappa^+$ and $\kappa^-$ denote the two \emph{end-points} of channel $\kappa$~\cite{DBLP:journals/acta/GayH05}.
Suppose now that $R$ simply represents an upgrade process, which is ready to synchronize with $r$, the location in which $S$ resides: 
%$$R = \adaptn{r}{NewS(\mathsf{X})}$$
$$R = \adapt{r}{NewS}{\mathsf{X}}$$
From $\mathsf{Sys}'$, an update on $r$ would be  highly inconvenient for at least two reasons:
\begin{enumerate}[(a)]
\item First, since $r$ contains the local server behavior for an already established session, 
a careless update action on $r$ could potentially discard such behavior. This would leave the client in $l_1$ without a partner---the  protocol agreed upon session establishment would not be respected. 
\item Second, since $r$ contains also the actual service definition $S$, an undisciplined 
update action on $r$ could 
affect the service on $a$ in a variety of ways---for instance, it could destroy it. 
This clearly goes against the expected nature of services, which should be always available. 
\end{enumerate}

\noindent Above, item (a) concerns our intended notion of consistency, which ensures that any update actions on $r$
(such as those involving $R$ above) are only enabled  when $r$ contains no active sessions. 
Closely related, item (b) concerns a most desirable principle for services, namely that ``services should always be available in multiple copies''---this is the Service Channel Principle (SCP) given in~\cite{DBLP:conf/esop/CarboneHY07}.


\paragraph{Contributions} The main contribution of this paper is a session typed framework with runtime adaptation.
 Our framework lies upon two main technical ingredients:
\begin{enumerate}[(1)]
%\item generalizing the operational semantics of~\cite{DBLP:conf/ppdp/GarraldaCD06}
%so as to account for adaptation in \emph{arbitrary process hierarchies}; 
\item An \emph{operational semantics} for  our session language with located and update processes~\cite{BGPZFMOODS}.
The semantics enables adaptation actions within  \emph{arbitrary process hierarchies} and, following~\cite{DBLP:conf/ppdp/GarraldaCD06}, 
endows each located process with a suitable \emph{runtime annotation}, which describes its active session behavior.
Runtime annotations for locations are key in avoiding undesirable update actions such as the described in~(a) above.

%conservatively extending the typing system in~\cite{DBLP:conf/ppdp/GarraldaCD06}, so as to be able to reason about \emph{process interfaces}.
\item A \emph{typing system} which extends existing session type systems~\cite{DBLP:journals/entcs/YoshidaV07,DBLP:conf/ppdp/GarraldaCD06}
with the notion of \emph{interface}, which allows\done\todo[B25.]{Fixed. Please check} for simple and intuitive static checking rules for evolvability constructs. 
In particular, interfaces are essential to rule out careless updates such as the described in (b) above.
This typing system provides a static analysis technique for ensuring not only
\emph{safety}\done\todo[B26.]{Fixed, please check}, i.e., absence of communication errors at runtime, but also 
consistency, as described above.
\end{enumerate}

%Ultimately, this last step is what realizes a form of \emph{typeful adaptation}, which contrasts with the untyped adaptation in~\cite{BGPZFMOODS}.  Well-typed processes 
%in our framework
%satisfy basic correctness guarantees (formalized as a Subject Reduction result), 
%which entails consistency for session-typed processes %that
%with runtime adaptation mechanisms.
%
%\jp{Perhaps adding an example of 'wrong' updates/consistency, to be addressed via static analysis?}


%\jp{This paragraph fits better at the end...}

\noindent To the best of our knowledge, our framework is the first in amalgamating structured communications and runtime adaptation from a session types perspective (either binary or multiparty).

\paragraph{Organization}
%The paper is structured as follows.
%Next, in \S\,\ref{sec:syn}, we 
The following section introduces our process language, a session $\pi$-calculus with adaptable processes.
In \S\,\ref{s:types} our session type system is presented; 
its main properties, namely  safety and consistency, 
are defined and investigated in~\S\,\ref{sec:res}. 
The typed approach is illustrated via examples in~\S\,\ref{sec:exam}, where the client/server scenario discussed above is revisited.
Extensions and enhancements for our framework are discussed in~\S\,\ref{sec:disc}:
they concern the runtime adaptation of processes with active sessions, and the incorporation of recursive types and subtyping.
%in particular refinements for our notion of  interfaces, are discussed in 
%\S\,\ref{sec:int}.
%\S\,\ref{sec:recsub}.
%Some perspectives for enhanced updates are outlined .
Finally, \S\,\ref{sec:rw} discusses related work and \S\,\ref{sec:conc} collects some concluding remarks.

This paper is a revised version of the conference paper~\cite{DBLP:conf/sac/GiustoP13}, extended 
with further examples and discussions.\done\todo[B2.]{We have reduced this paragraph, and moved the rest to the related work section.} %\footnote{Process $\adapt{l}{Q}{X}$ was written $l\{Q(\mathsf{X})\}$ in \cite{DBLP:conf/sac/GiustoP13}.}
%In particular, \S\,\ref{ss:examp}, which illustrates runtime adaptation patterns
%in an untyped setting, is new to this presentation, whereas 
% \S\,\ref{sec:exam}, \S\,\ref{sec:int}, and \S\,\ref{sec:rw} have been expanded significantly.
 See \S\,\ref{sec:rw} for further comparisons with respect to~\cite{DBLP:conf/sac/GiustoP13}. 
This presentation also contains the proofs of the main technical results; most of them are collected in the Appendix.


